|
The device driver is a program which allows the software or higher-level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also mediate the communication between the operating system kernel and the devices below. Usually the operating systems comes with a support for the common device drivers and usually the hardware vendors provide the device driver for their hardware devices for most platforms. The aggressive scaling of the hardware devices and the complex software components has made the device driver development process cumbersome and complex. When the size and functionality of the drivers started increasing the device drivers became a key factor in defining the reliability of the system. This has created an incentive towards automatic synthesis and verification of device drivers. This article sheds some light into some approaches in synthesis and verification of device drivers. ==Motivation for automatic driver synthesis and verification== The device drivers are the principal failing component in most systems. The Berkeley Open Infrastructure for Network Computing (BOINC) project found that OS crashes are predominantly caused by poorly written device driver code.〔Archana Ganapathi, Viji Ganapathi and David Patterson. "Windows XP kernel crash analysis". In Proceedings of the 2006 Large Installation System Administration Conference, 2006.〕 In Windows XP, drivers account for 85% of the reported failures. In the Linux kernel 2.4.1 device driver code accounts for about 70% of the code size.〔A. Chou, J. Yang, B. Chelf, S. Hallem and D. Engler. An Empirical Study of Operating Systems Errors. In SOSP, 2001〕 The driver fault can crash the whole system as it is running in the kernel mode. These findings resulted in various methodologies and techniques for verification of device drivers. An alternative was to develop techniques which can synthesize device drivers robustly. Less human interaction in the development process and proper specification of the device and operating systems can lead to more reliable drivers. The other motivation for driver synthesis, is the large number of flavors of operating systems and device combinations. Each of these has its own set of input/output control and specifications which makes support of hardware devices on each of the operating systems difficult. So the ability to use a device with an operating system requires the availability of corresponding device driver combination. Hardware vendors usually supply the drivers for Windows, Linux and Mac OS but due to the high development or porting costs and technical support difficulties they are unable to provide drivers on all platforms. An automated synthesis technique can help the vendors in providing drivers to support any devices on any operating system. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Device driver synthesis and verification」の詳細全文を読む スポンサード リンク
|